Lean 型クラス

Lean 型クラス(Lean type class)

code:lean

class Group (G : Type) where

op : G -> G -> G

assoc : ∀ (a b c : G), op (op a b) c = op a (op b c)

unit : { e : G // ∀ (x : G) }, op e x = x ∧ (op x e) = x

inv : ∀ (x : G), { y : G // (op x y) = unit ∧ op y x = unit　}

確認用

Q. Lean 型クラス

参考

調査用

Wikipedia.icon

Wikipedia.icon